Inference at * 1 1 1 1 1 
Iof proof for Lemma nth tl is fseg:

.....falsecase..... NILNIL

1. T : Type
2. L1 : T List
3. T List
4. T
5. v : T List
6. L1 = nth_tl(||v||;v @ L1)
7. 0 < (||v||+1)
  L1 = nth_tl((||v||+1) - 1;v @ L1) 

latex

 by ((ArithSimp 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	, T, x:A. B(x), x:AB(x), , n+m, #$n, nth_tl(n;as), ||as||, as @ bs, a < b, type List, Type, s = t, n - m, True, t  T
Lemmas	nth tl wf, squash wf, true wf, append wf